Nuprl Lemma : choicef_lemma
12,41
postcript
pdf
%xm
:XM,
T
:Type,
P
:(
T
). (
a
:
T
.
P
(
a
))
P
(
x
:
T
.
P
(
x
))
latex
ProofTree
origin
%xm:XM, T:Type, P:(T
). (
a:T. P(a)) 
P(
x:T. P(x))
%xm:XM, T:Type, P:(T). (a:T. P(a)) P(x:T. P(x))